$\forall$$M$:MsgA, $l$:IdLnk, ${\it mss}$:($M$.Msg List). withlnk($l$;${\it mss}$) $\in$ ((${\it tg}$:Id $\times$ $M$.dout($l$,${\it tg}$)) List)